|
In mathematical logic, a ground term of a formal system is a term that does not contain any free variables. Similarly, a ground formula is a formula that does not contain any free variables. In first-order logic with identity, the sentence ''x'' (''x''=''x'') is a ground formula. A ground expression is a ground term or ground formula. == Examples == Consider the following expressions from first order logic over a signature containing a constant symbol 0 for the number 0, a unary function symbol ''s'' for the successor function and a binary function symbol + for addition. * ''s''(0), ''s''(''s''(0)), ''s''(''s''(''s''(0))) ... are ground terms; * 0+1, 0+1+1, ... are ground terms. * x+''s''(1) and ''s''(x) are terms, but not ground terms; * ''s''(0)=1 and 0+0=0 are ground formulae; * ''s''(1) and ∀x: (''s''(x)+1=''s''(''s''(x))) are ground expressions. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Ground expression」の詳細全文を読む スポンサード リンク
|